By securing the program it should be understood that in this document, the program is written in order to guarantee operating in accordance with the specifications or the operating constraints, or that some of its (local) properties (as defined below) are proven correct.
In an automatic controlling equipment of a system, such as a rocket or a train, it is necessary to ensure that the program executes exactly within its operating range in order to prevent to jeopardize the system or the environment thereof.
This appears as particularly important in complex systems because these, owing to their complexity, are very difficult to analyze by specialists. This difficulty can be illustrated by the accident that occurred during the first flight of the Ariane V rocket, which after expertise, turned out to be due to a thrust engine control computer. In fact, the latter was programmed for the previous generation rocket Ariane IV that, less powerful, had less strong accelerations. The transfer of this computer onto the Ariane V rocket without taking this new parameter into consideration led the latter to receive acceleration data, which triggered an unanticipated register overflow and a motor control malfunction.
Thus, it appears extremely important, for critical systems that the execution domain as well as the execution within this domain to be perfectly defined, documented and verified.
The currently-used techniques are mainly based on mathematical rules based on first-order logic, or high-order logic such as Coq. They consist in using specific programming languages with software tools which will attempt to prove, in the mathematical sense. These software programs are called in the literature “provers”.
The operation of these provers fundamentally consists in transcribing the studied program into logical assertions (i.e. “proof obligations”) to be proven. Another possibility is to use the logical language itself, such as Coq, in order to describe the programs, express the properties and prove, thus avoiding the need for transformation into logical assertions.
However, it appears that the complexity, in the algorithmic sense, of the search for logic proofs increases faster than the complexity of the studied program. In the case of a computer-assisted proof, it appears that the user finds it difficult to use the intuition he has for the good operating of the program, in order to guide the prover. These techniques thus, become very difficult and high consumers of time and resources as soon as working on critical and complicated programs, such as control programs and/or complex system where security is involved. Thus, while the need has become more and more important and research teams have been working on this subject for at least 30 years, these proof technologies have remained in the laboratories or are used in extremely demanding sectors regarding operational security such as aerospace or rail with, hence, in this case, a software architecture which makes it possible to cut these programs into sub-assemblies that can be managed by the provers.
It would be thus advantageous to obtain a method for securing a program which would be adapted for usage on complex programs. From now on, the term “proof” (or “formal proof”) will be used as a synonym for “formal verification”, i.e. verification based on formal methods in general, and the term “logic proof” for the specific case of proof in classic logic systems (predicate logic, higher-order logic).